home *** CD-ROM | disk | FTP | other *** search
/ Language/OS - Multiplatform Resource Library / LANGUAGE OS.iso / quintus / quintus0.lha / work / auxiliary_2.06.2 < prev    next >
Text File  |  1992-04-03  |  27KB  |  897 lines
  1. %%% AUXILIARIES
  2. %%% version 2.00.1 (based on auxilary_19.3)
  3. %%%   added write_line/5
  4. %%% version 2.00.9
  5. %%%   modified literal_depth and literal_size to support variable literals
  6. %%% version 2.01.0
  7. %%%   checked clause priority after each hyper-link
  8. %%% version 2.01.6
  9. %%%   fixed bug in literal_size which caused not to be counted
  10. %%% version 2.01.8
  11. %%%   added transformed form of all non-input equations before hyper-linking
  12. %%%   fixed bug in duplicate_clause_C
  13. %%% version 2.01.9
  14. %%%   optimized term rewriting
  15. %%% version 2.02.1
  16. %%%   asserted over_priohm if priority exceeded during rewriting or
  17. %%%     hyper-linking
  18. %%% version 2.02.2
  19. %%%   deleted pulled out form when rewriting asserted clause
  20. %%% version 2.02.3
  21. %%%   deleted pulled out form of clauses whose priority is too large
  22. %%% version 2.03.4
  23. %%%   incorporated changes made to clin V1 between 7/31/90 and 10/18/90 which
  24. %%%     are visible externally -- changes to comments, predicate names, and
  25. %%%     variable names are not incorporated
  26. %%% version 2.04.0
  27. %%%   logically erased nuclei while hyper-linking
  28. %%%   fixed bug with "outhllits"
  29. %%% version 2.04.3
  30. %%%   fixed bug in logically_erase_clause_C
  31. %%% version 2.04.4
  32. %%%   erased equation associated with rewrite rule only if equation's priority
  33. %%%     exceeded priority bound
  34. %%% version 2.04.5
  35. %%%   added duplicate_clauses
  36. %%% version 2.04.6
  37. %%%   added fixed_priority
  38. %%% version 2.04.7
  39. %%%   modified logically_erase_clause_C_prio so that it only erases non-input
  40. %%%     clauses
  41. %%%   modified erase_clause_HM_prio so that it only erases non-input clauses
  42. %%%   modified erase_clause_T_prio so that it only erases non-input clauses
  43. %%% version 2.04.8
  44. %%%   added duplicate_repeated_replace_rule
  45. %%% version 2.05.3
  46. %%%   added support for Quintus Prolog
  47. %%% version 2.05.6
  48. %%%   added print after clause generation
  49. %%% version 2.05.8
  50. %%%   added write_line/4
  51. %%%   added ttyflush to write_line
  52. %%% version 2.06.0
  53. %%%   added instance_clause_C/2
  54. %%%   added write_line/6
  55. %%%   added check_unit_conflict_C/1
  56. %%%   added check_unit_conflict_HM/1
  57. %%% version 2.06.1
  58. %%%   fixed bug in check_unit_conflict_C/1 and check_unit_conflict_HM/1
  59. %%%   added duplicate_once_replace_rule/2
  60. %%% version 2.06.2
  61. %%%   modified rewrite_rule_ref/2 to work with linearized rwr
  62. %%%
  63. %%% COMPARISON
  64. %%%
  65.      max_CS_ind(sp(S11,S12,S13),sp(S21,S22,S23),sp(S31,S32,S33),Up) :-
  66.     binary_max_ind(S11,S21,S31,Up),
  67.     binary_max_ind(S12,S22,S32,Up),
  68.     binary_max_ind(S13,S23,S33,Up).
  69.  
  70. %%% Only for binary comparison.
  71.      binary_max_ind(0,1,1,u) :- !.
  72.      binary_max_ind(Y,_,Y,Up).
  73.  
  74. %%% Only for binary comparison.
  75.      binary_min_ind(1,0,0,u) :- !.
  76.      binary_min_ind(Y,_,Y,Up).
  77.  
  78. %%% Take maximum of CS without indicator.
  79.      max_CS(sp(S11,S12,S13),sp(S21,S22,S23),sp(S31,S32,S33)) :-
  80.     binary_max(S11,S21,S31),
  81.     binary_max(S12,S22,S32),
  82.     binary_max(S13,S23,S33).
  83.  
  84. %%% Only for binary comparison.
  85.      binary_max(0,1,1) :- !.
  86.      binary_max(Y,_,Y).
  87.  
  88. %%% Only for binary comparison.
  89.      binary_min(1,0,0) :- !.
  90.      binary_min(Y,_,Y).
  91.  
  92. %%% For any value.
  93.      min_ind(V1,V2,V2,u) :- V2 < V1, !.
  94.      min_ind(V1,_,V1,Up).
  95.  
  96. %%% For any value.
  97.      max_ind(V1,V2,V2,u) :- V2 > V1, !.
  98.      max_ind(V1,_,V1,Up).
  99.  
  100. %%% Compare two CR's. 
  101.      min_CR_ind(ds(R11,R12,R13),ds(R21,R22,R23),ds(R31,R32,R33),Up) :-
  102.     min_ind(R11,R21,R31,Up),
  103.     min_ind(R12,R22,R32,Up),
  104.     min_ind(R13,R23,R33,Up).
  105.  
  106. %%% Minimum of CR without indicator.
  107.      min_CR(ds(R11,R12,R13),ds(R21,R22,R23),ds(R31,R32,R33)) :-
  108.     minimum(R11,R21,R31),
  109.     minimum(R12,R22,R32),
  110.     minimum(R13,R23,R33).
  111.  
  112. %%% Minimum of Fs with indicator.
  113.      min_Flags_ind([F1|Fs1],[F2|Fs2],[F3|Fs3],Up) :-
  114.     binary_min_ind(F1,F2,F3,Up), !,
  115.     min_Flags_ind(Fs1,Fs2,Fs3,Up).
  116.      min_Flags_ind([],[],[],Up).
  117.  
  118. %%% RELATED ROUTINES
  119. %%%
  120. %%% calculate the size of a clause.
  121.      clause_size(C,S) :- clause_size(C,0,S).
  122.      clause_size([L|Ls],S1,S2) :-
  123.     term_size(L,SL),
  124.     SM is S1 + SL, !,
  125.     clause_size(Ls,SM,S2).
  126.      clause_size([],S,S).
  127.  
  128. %%% calculate the size of a clause for sliding priority.
  129. %%% don't count not.
  130.      clause_size_sp(C,S) :- clause_size_sp(C,0,S).
  131.      clause_size_sp([L|Ls],S1,S2) :-
  132.     literal_size(L,SL),
  133.     SM is S1 + SL, !,
  134.     clause_size_sp(Ls,SM,S2).
  135.      clause_size_sp([],S,S).
  136.  
  137. %%% literal_depth computes the depth of a literal. It doesn't count "not".
  138. %%%     For example, f(g(a)) has depth 2, while not f(g(a)) also has 
  139. %%%    depth 2. The reason for this is that we want them having the 
  140. %%%    same importance to the priority consideration. Since we use
  141. %%%    matching strategy, a positive literal should be matched with a 
  142. %%%    negative literal.
  143.      literal_depth(X,D) :-
  144.     nonvar(X), X=not(Y), !,
  145.     term_depth_ns(Y,D), !.
  146.      literal_depth(X,D) :-
  147.     term_depth_ns(X,D), !.
  148.  
  149. %%% Calculate the depth of a term for sliding priority.
  150.      term_depth_ns(X,D) :- var(X), var_depth(X,D), !.
  151.      term_depth_ns(X,D) :- nonvar_depth_weight(X,D), !.
  152.      term_depth_ns(X,0) :- atomic(X), !.
  153.      term_depth_ns(X,D) :-
  154.     X =.. [F|Args],
  155.     arg_depth_ns(Args,0,Darg),
  156.     D is Darg + 1, !.
  157.      arg_depth_ns([A1|As],Din,Dout) :-
  158.     term_depth_ns(A1,D1),
  159.     maximum(Din,D1,D2), !,
  160.     arg_depth_ns(As,D2,Dout).
  161.      arg_depth_ns([],D,D).
  162.  
  163. %%% Calculate depth for a variable.
  164. %%% If we have var_depth_weight(T,D) in database, then the weight is D.
  165. %%% Otherwise it is 0.
  166.      var_depth(X,D) :-
  167.     var_depth_weight(X,D), !.
  168.      var_depth(X,0).
  169.     
  170. %%% literal_size calculates the size of a literal. Do not count not.
  171.      literal_size(X,S) :- 
  172.     nonvar(X), X=not(Y), !,
  173.     term_size_ns(Y,S), !.
  174.      literal_size(X,S) :- 
  175.     term_size_ns(X,S), !.
  176.  
  177. %%% Calculate the size of a term for sliding priority.
  178.      term_size_ns(Term,Size) :-
  179.     term_size_ns(Term,0,Size).
  180.      term_size_ns(Term,Size1,Size2) :-
  181.     var(Term), var_size(Term,W), Size2 is Size1 + W, !.
  182.      term_size_ns(Term,Size1,Size2) :-
  183.     nonvar_size_weight(Term,W), 
  184.     Size2 is Size1 + W, !.
  185.      term_size_ns(Term,Size1,Size2) :-
  186.     atomic(Term),
  187.     Size2 is Size1 + 1, !.
  188.      term_size_ns(Term,Size1,Size2) :-
  189.     functor(Term,F,N),
  190.     SizeM is Size1 + 1,
  191.     args_size_ns(Term,0,N,SizeM,Size2).
  192.  
  193.      args_size_ns(Term,N1,N2,SizeI,SizeO) :-
  194.     NN is N1 + 1,
  195.     NN =< N2,
  196.     arg(NN,Term,Arg),
  197.     term_size_ns(Arg,SizeI,SizeM),
  198.     !,
  199.     args_size_ns(Term,NN,N2,SizeM,SizeO).
  200.      args_size_ns(Term,N,N,SizeO,SizeO).
  201.  
  202. %%% Calculate size for a variable.
  203. %%% If we have var_size_weight(T,W) in database, then the weight is W.
  204. %%% Otherwise it is 1.
  205.      var_size(X,W) :-
  206.     var_size_weight(X,W), !.
  207.      var_size(X,1).
  208.     
  209. %%% Calculate priority for a clause.
  210.      calculate_priority_clause(_,_,_,pr(0,0,0,0,0)) :-
  211.     not(fixed_priority),
  212.     not(slidepriority),
  213.     !.
  214.      calculate_priority_clause(Cn1,CS1,CR1,pr(PS,PD,PL,PR,P)) :-
  215.     depth_coef(DCoef),
  216.     size_coef(SCoef),
  217.     literal_coef(LCoef),
  218.     relevance_coef(RCoef),
  219.     priority_PS(SCoef,Cn1,PS),
  220.     priority_PD(DCoef,Cn1,PD),
  221.     priority_PL(LCoef,Cn1,CS1,PL),
  222.     priority_PR(RCoef,CR1,PR),
  223.     priority_clause(PS,PD,PL,PR,P), !.
  224.  
  225. %%% calculate the priority of a clause.
  226. %%% The priority is rounded to integer.
  227. %%% The formula is 
  228. %%%     priority = max(Cs*S, Cd*d, Cr*max(B+F,U), Cl*l)
  229. %%%
  230.      priority_clause(PS,PD,PL,PR,P) :-
  231.     \+ sum_of_measures,
  232.     maximum(PS,PD,X1),
  233.     maximum(X1,PL,X2),
  234.     maximum(X2,PR,P), !.
  235.      priority_clause(PS,PD,PL,PR,P) :-
  236.     P is PS + PD + PL + PR.
  237.  
  238. %%% calculate the PS part of priority.
  239.      priority_PS(SCoef,Cn1,PS) :-
  240.     max_clausesize_sp(Cn1,MLSize),
  241.     Temp is SCoef * MLSize,
  242.     floor(Temp,PS).
  243.  
  244. %%% If all literal size is asserted, count all literals.
  245. %%% Otherwise, use the maximum literal size.
  246.      max_clausesize_sp(Cn1,MLSize) :-
  247.     size_by_clause,
  248.     clause_size_sp(Cn1,MLSize), !.
  249.      max_clausesize_sp(Cn1,MLSize) :-
  250.     maxliteral_size(Cn1,MLSize).
  251.  
  252. %%% calculate the PD part of priority.
  253.      priority_PD(DCoef,Cn1,PD) :-
  254.     clause_depth(Cn1,DClause),
  255.     Temp is DCoef * DClause,
  256.     floor(Temp,PD).
  257.  
  258. %%% calculate the PL part of priority.
  259.      priority_PL(LCoef,Cn1,CS1,PL) :-
  260.     numberof_literals_sp(Cn1,CS1,NLiterals),
  261.     Temp is LCoef * NLiterals,
  262.     floor(Temp,PL).
  263.  
  264. %%% calculate priority part PR.
  265.      priority_PR(RCoef,ds(R11,R12,R13),PR) :-
  266.     YY is R12 + R13,
  267.     maximum(YY,R11,Max2),
  268.     Temp is RCoef * Max2,
  269.     floor(Temp,PR).
  270.  
  271.      priority_NewPR(_,0) :-
  272.     not(fixed_priority),
  273.     not(slidepriority),
  274.     !.
  275.      priority_NewPR(CR3,PR3) :-
  276.     relevance_coef(RCoef),
  277.     priority_PR(RCoef,CR3,PR3), !.
  278.  
  279. %%% calculate the depth of a clause.
  280. %%% The depth of a clause is the maximum of the depths of all its literals.
  281.      clause_depth(C,S) :- clause_depth(C,0,S).
  282.      clause_depth([L|Ls],D1,D2) :-
  283.     literal_depth(L,DTerm),
  284.     maximum(DTerm,D1,DMid), !,
  285.     clause_depth(Ls,DMid,D2).
  286.      clause_depth([],D2,D2).
  287.  
  288. %%% calculate the number of literals in a clause for sliding priority use.
  289.      numberof_literals_sp(Cn1,_,NLiterals) :-
  290.     count_all_literals,
  291.     length(Cn1,NLiterals), !.
  292.      numberof_literals_sp(Cn1,sp(_,_,1),NLiterals) :-
  293.     length(Cn1,NLiterals), !.    % length is a system predicate.
  294.      numberof_literals_sp(Cn1,_,NLiterals) :-
  295.     number_poslits(Cn1,0,NLiterals).
  296.  
  297. %%% if all negative clause, count it as 1.
  298.      number_poslits([L1|Ls1],N,NLiterals) :-
  299.     \+ negative_lit(L1),
  300.     NN is N + 1, !,
  301.     number_poslits(Ls1,NN,NLiterals).
  302.      number_poslits([_|Ls1],N,NLiterals) :-
  303.     !,
  304.     number_poslits(Ls1,N,NLiterals).
  305.      number_poslits([],0,1) :- !.
  306.      number_poslits([],N,N).
  307.  
  308. %%% calculate the size of largest literal in a clause.
  309. %%% We don't count 'not'.
  310.      maxliteral_size(Cn1,MLSize) :-
  311.     maxliteral_size(Cn1,0,MLSize).
  312.      maxliteral_size([L|Ls],S1,S2) :-
  313.     literal_size(L,X),
  314.     maximum(X,S1,SM), !,
  315.     maxliteral_size(Ls,SM,S2).
  316.      maxliteral_size([],S2,S2).
  317.  
  318. %%% Check if a given clause is a negative clause.
  319.      negclause([P1|Ps]) :-
  320.     negative_lit(P1), !,
  321.     negclause(Ps).
  322.      negclause([]).
  323.  
  324. %%% Check if a given clause is a positive clause.
  325.      posclause([P1|Ps]) :-
  326.     \+ negative_lit(P1), !,
  327.     posclause(Ps).
  328.      posclause([]).
  329.  
  330. %%% Fails if the clause is neither positive nor negative.
  331. %%% Returns with flag of 'n' if the clause is negative.
  332. %%% Returns with flag of 'p' if the clause is positive.
  333.      pn_clause([L|Ls],n) :-
  334.     negative_lit(L),
  335.     !,
  336.     pn_clause(Ls,n).
  337.      pn_clause([L|Ls],p) :-
  338.     \+ negative_lit(L),
  339.     !,
  340.     pn_clause(Ls,p).
  341.      pn_clause([],_).
  342.  
  343. %%% Note that this can only be used in literals, not for terms.
  344. %%% negative_lit is for determining a literal of the form LP is
  345. %%% negative.
  346.      negative_lit(not(_)) :- !.
  347.  
  348. %%% initialize num for numerically labelling output clauses.
  349.      init_num :-
  350.     retract(num(_)),
  351.         assert(num(0)), !.
  352.      init_num :-
  353.         assert(num(0)), !.
  354.  
  355. %%% take the content of num plus one as output. Also increment num in database.
  356.      next_num(N) :-
  357.     retract(num(X)),
  358.     N is X + 1,
  359.     assert(num(N)), !.
  360.      next_num(1) :-
  361.     assert(num(1)), !.
  362.  
  363. %%% PRINTING ROUTINES:
  364. %%%
  365.  
  366. %%% print out clauses after hyper-matching.
  367.      print_ahm :-
  368.     outCahl,
  369.     write_line(5,'Clause set after hyper-linking :'),
  370.     init_num,
  371.     print_sentC, !.
  372.      print_ahm.
  373.  
  374. %%% print out clauses before doing unit subsumption/simplification.
  375.      print_busentC :-
  376.     outCagen,
  377.     write_line(5,'Clause set after clause generation :'),
  378.     init_num,
  379.     print_sentC, !.
  380.      print_busentC.
  381.  
  382.      print_sentC :-
  383.     sent_C(cl(_,_,by(Cn1,V11,V11,V1,_),_,CS1,CR1,_,CF1,_)),
  384.     printsentC_2(Cn1,V1,CS1,CR1,CF1),
  385.     fail.
  386.      print_sentC.
  387.  
  388. %%% print out clauses after doing unit simplification.
  389.      print_ausentC :-
  390.     outCasimp,
  391.     write_line(5,'Clause set after simplification :'),
  392.     init_num,
  393.     print_sentC, !.
  394.      print_ausentC.
  395.  
  396.      printsentC_2(Cn1,V1,CS1,CR1,CF1) :-
  397.     next_num(N),
  398.     write_numberedline_head(10,N,'.'),
  399.     print_clause(2,15,Cn1,V1,CS1,CR1,CF1), !. 
  400.  
  401.      printsentC_2(Cn1,V1,CS1,CR1) :-
  402.     next_num(N),
  403.     write_numberedline_head(10,N,'.'),
  404.     print_clause(2,15,Cn1,V1,CS1,CR1), !. 
  405.  
  406. %%% print out clauses after instance deletion. 
  407.      print_after_instdel :-
  408.         outCainst,         
  409.         write_line(5,'Clause set after instance deletion :'), 
  410.         init_num, 
  411.         print_sentC, !.  
  412.      print_after_instdel.
  413.  
  414. %%% print out clauses after clause generation. 
  415.      print_after_clause_generation :-
  416.         outCacg,         
  417.         write_line(5,'Clause set after clause generation :'), 
  418.         init_num, 
  419.         print_sentC, !.  
  420.      print_after_clause_generation.
  421.  
  422. %%% print out fully matched set.
  423.      print_fms(FMS) :-
  424.     outfls,
  425.     write_line(5,'FLS set are :'),
  426.     print_clause_list(FMS), !.
  427.      print_fms(_).
  428.  
  429.      print_clause_list(FMS) :-
  430.     init_num,
  431.     print_clause_list_1(FMS).
  432.  
  433.      print_clause_list_1([F|FMS]) :-
  434.     next_num(N),
  435.     write_numberedline_head(10,N,'.'),
  436.     write_line(2,F), !,
  437.     print_clause_list_1(FMS).
  438.      print_clause_list_1([]).
  439.  
  440. %%% print out a hyper-match.
  441.      print_HM(Cn1,V1,CS1,CR1,CF1) :- 
  442.     outinst,
  443.     print_clause(10,15,Cn1,V1,CS1,CR1,CF1), !.
  444.      print_HM(_,_,_,_,_) :- !.
  445.  
  446. %%% print out nucleus.
  447.      print_nucleus(Cn1,V1,CS1,CR1,CF1) :-
  448.     outinst,
  449.     write_line(5,'Current nucleus is :'),
  450.     print_clause(10,15,Cn1,V1,CS1,CR1,CF1),
  451.     write_line(5,'New instances obtained from the nucleus are :'), !.
  452.      print_nucleus(_,_,_,_,_) :- !.
  453.  
  454.      print_clause(N1,N2,Cn1,V1,CS1,CR1,CF1) :-
  455.     print_clause_2(N1,Cn1,V1),
  456.     print_SR(N2,CS1,CR1,CF1), !.
  457.  
  458.      print_clause(N1,N2,Cn1,V1,CS1,CR1) :-
  459.     print_clause_2(N1,Cn1,V1),
  460.     print_SR(N2,CS1,CR1), !.
  461.  
  462.      print_clause_2(N,Cn1,V1) :-
  463.     var_list(V1),
  464.     write_line(N,Cn1), fail.
  465.      print_clause_2(_,_,_).
  466.  
  467. %%% print out distances
  468.      print_SR(N,CS1,CR1,CF1) :- 
  469.     tab(N), write(CS1),write(', '),write(CR1),write(', '),write(CF1),nl.
  470.  
  471.      print_SR(N,CS1,CR1) :- 
  472.     tab(N), write(CS1),write(', '),write(CR1),nl.
  473.  
  474. %%% print out literal list.
  475.      print_litsall :-
  476.     outhllits,
  477.     write_line(5,'Lit_G list in hyper-linking:'),
  478.     init_num,
  479.     print_litG_2, 
  480.     write_line(5,'Lit_S list in hyper-linking:'),
  481.     init_num,
  482.     print_litS_2, 
  483.     !.
  484.      print_litsall.
  485.  
  486. %%% Print out general literal list.
  487.      print_litG_2 :-
  488.     lit_G(_,lby(Ln1,V11,V11,V1),CS1,CR1),
  489.     printsentC_2(Ln1,V1,CS1,CR1),
  490.     fail.
  491.      print_litG_2.
  492.  
  493. %%% Print out supported literal list.
  494.      print_litS_2 :-
  495.     lit_S(_,lby(Ln1,V11,V11,V1),CS1,CR1),
  496.     printsentC_2(Ln1,V1,CS1,CR1),
  497.     fail.
  498.      print_litS_2.
  499.  
  500. %%% Write a line out.
  501.      write_line(N,Text) :-
  502.     tab(N),write(Text),nl,ttyflush,!.
  503.      write_line(N,Text,Object) :-
  504.     tab(N),write(Text),write(Object),nl,ttyflush,!.
  505.      write_line(N,Text,Object1,Object2) :-
  506.     tab(N),write(Text),write(Object1),write(Object2),nl,telling(File),
  507.     flush_output(File),!.
  508.      write_line(N,Text,Object1,Object2,Object3) :-
  509.     tab(N),write(Text),write(Object1),write(Object2),write(Object3),nl,
  510.     ttyflush,!.
  511.      write_line(N,Text,Object1,Object2,Object3,Object4) :-
  512.     tab(N),write(Text),write(Object1),write(Object2),write(Object3),
  513.     write(Object4),nl,ttyflush,!.
  514.  
  515. %%% write the head for a numbered line.
  516.      write_numberedline_head(T1,N,Text) :-
  517.     tab(T1),write(N),write(Text), !.
  518.  
  519. %%% Check the number of variables in a clause.
  520.      check_numbervars(V2,S) :-
  521.     \+ const_list(V2),
  522.     write_line(5,S),
  523.     assert_once(over_numvars), !, fail.
  524.      check_numbervars(_,_).
  525.  
  526. %%% Literals remaining -- 1.
  527. %%% Delete any literals with 1 in the corresponding position of another list.
  528.      literals_remain_1([1|Ns1],[_|Lns1],Cn2,1) :-
  529.     literals_remain_1(Ns1,Lns1,Cn2,1).
  530.      literals_remain_1([0|Ns1],[Ln1|Lns1],[Ln1|Lns2],DF) :-
  531.     literals_remain_1(Ns1,Lns1,Lns2,DF).
  532.      literals_remain_1([],[],[],_).
  533.  
  534. %%% Literals remaining -- 2.
  535. %%% Delete any literals with 1 in the corresponding position of another list.
  536.      literals_remain_2([1|Ns1],[_|Lns1],[_|Wns1],Cn2,W2,1) :-
  537.     literals_remain_2(Ns1,Lns1,Wns1,Cn2,W2,1).
  538.      literals_remain_2([0|Ns1],[Ln1|Lns1],[Wn1|Wns1],[Ln1|Lns2],
  539.         [Wn1|Wns2],DF) :-
  540.     literals_remain_2(Ns1,Lns1,Wns1,Lns2,Wns2,DF).
  541.      literals_remain_2([],[],[],[],[],_).
  542.  
  543. %%% Literals remaining -- 3.
  544. %%% Delete any literals with 1 in the corresponding position of another list.
  545.      literals_remain_3([1|Ns1],[_|Lns1],[_|Wns1],[_|Fns1],Cn2,W2,F2,1) :-
  546.     literals_remain_3(Ns1,Lns1,Wns1,Fns1,Cn2,W2,F2,1).
  547.      literals_remain_3([0|Ns1],[Ln1|Lns1],[Wn1|Wns1],[Fn1|Fns1],
  548.         [Ln1|Lns2],[Wn1|Wns2],[Fn1|Fns2],DF) :-
  549.     literals_remain_3(Ns1,Lns1,Wns1,Fns1,Lns2,Wns2,Fns2,DF).
  550.      literals_remain_3([],[],[],[],[],[],[],_).
  551.  
  552. %%% Clause remaining -- 1.
  553. %%% Keep literals if the ordinal number of these literals are listed in
  554. %%%    another list.
  555.      clause_remain_1([N1|Flags],N1,[Ln1|Lns1],[Ln1|Lns2]) :-
  556.     N2 is N1 + 1, !,
  557.     clause_remain_1(Flags,N2,Lns1,Lns2).
  558.      clause_remain_1(Flags,N1,[_|Lns1],Lns2) :-
  559.     N2 is N1 + 1, !,
  560.     clause_remain_1(Flags,N2,Lns1,Lns2).
  561.      clause_remain_1([],_,_,[]).
  562.  
  563. %%% Clause remaining -- 2.
  564. %%% Keep literals if the ordinal number of these literals are listed in
  565. %%%    another list.
  566.      clause_remain_2([N1|Flags],N1,[Ln1|Lns1],[Wn1|Wns1],
  567.         [Ln1|Lns2],[Wn1|Wns2]) :-
  568.     N2 is N1 + 1, !,
  569.     clause_remain_2(Flags,N2,Lns1,Wns1,Lns2,Wns2).
  570.      clause_remain_2(Flags,N1,[_|Lns1],[_|Wns1],Lns2,Wns2) :-
  571.     N2 is N1 + 1, !,
  572.     clause_remain_2(Flags,N2,Lns1,Wns1,Lns2,Wns2).
  573.      clause_remain_2([],_,_,_,[],[]).
  574.  
  575. %%% Clause remaining -- 3.
  576. %%% Keep literals if the ordinal number of these literals are listed in
  577. %%%    another list.
  578.      clause_remain_3([N1|Flags],N1,[Ln1|Lns1],[Wn1|Wns1],[Fn1|Fns1],
  579.         [Ln1|Lns2],[Wn1|Wns2],[Fn1|Fns2]) :-
  580.     N2 is N1 + 1, !,
  581.     clause_remain_3(Flags,N2,Lns1,Wns1,Fns1,Lns2,Wns2,Fns2).
  582.      clause_remain_3(Flags,N1,[_|Lns1],[_|Wns1],[_|Fns1],Lns2,Wns2,Fns2) :-
  583.     N2 is N1 + 1, !,
  584.     clause_remain_3(Flags,N2,Lns1,Wns1,Fns1,Lns2,Wns2,Fns2).
  585.      clause_remain_3([],_,_,_,_,[],[],[]).
  586.  
  587.  
  588. %%% Duplicate deletions -- 1.
  589. %%% Delete duplicate literals in a clause.
  590.      delete_replicate_literals_1([L1|Lm],[L1|Ln]) :-
  591.          delete_replicate_literal_1(L1,Lm,Lx), !,
  592.          delete_replicate_literals_1(Lx,Ln).
  593.      delete_replicate_literals_1([],[]).
  594.  
  595.      delete_replicate_literal_1(L1,[L2|Lm],Lx) :-
  596.     L1 == L2, !,
  597.     delete_replicate_literal_1(L1,Lm,Lx).
  598.      delete_replicate_literal_1(L1,[L2|Lm],[L2|Lx]) :-
  599.     delete_replicate_literal_1(L1,Lm,Lx).
  600.      delete_replicate_literal_1(_,[],[]).
  601.  
  602. %%% Duplicate deletions -- 2.
  603. %%% Delete duplicate literals in a clause.
  604.      delete_replicate_literals_2([L1|Lm],[W1|Wm],[L1|Ln],[W1|Wn]) :-
  605.          delete_replicate_literal_2(L1,Lm,Wm,Lx,Wx), !,
  606.          delete_replicate_literals_2(Lx,Wx,Ln,Wn).
  607.      delete_replicate_literals_2([],[],[],[]).
  608.  
  609.      delete_replicate_literal_2(L1,[L2|Lm],[W2|Wm],Lx,Wx) :-
  610.     L1 == L2, !,
  611.     delete_replicate_literal_2(L1,Lm,Wm,Lx,Wx).
  612.      delete_replicate_literal_2(L1,[L2|Lm],[W2|Wm],[L2|Lx],[W2|Wx]) :-
  613.     delete_replicate_literal_2(L1,Lm,Wm,Lx,Wx).
  614.      delete_replicate_literal_2(_,[],[],[],[]).
  615.  
  616. %%% Duplicate deletions -- 3.
  617. %%% Delete duplicate literals in a clause.
  618.      delete_replicate_literals_3([L1|Lm],[W1|Wm],[F1|Fm],
  619.         [L1|Ln],[W1|Wn],[F1|Fn]) :-
  620.          delete_replicate_literal_3(L1,Lm,Wm,Fm,Lx,Wx,Fx), !,
  621.          delete_replicate_literals_3(Lx,Wx,Fx,Ln,Wn,Fn).
  622.      delete_replicate_literals_3([],[],[],[],[],[]).
  623.  
  624.      delete_replicate_literal_3(L1,[L2|Lm],[_|Wm],[_|Fm],Lx,Wx,Fx) :-
  625.     L1 == L2, !,
  626.     delete_replicate_literal_3(L1,Lm,Wm,Fm,Lx,Wx,Fx).
  627.      delete_replicate_literal_3(L1,[L2|Lm],[W2|Wm],[F2|Fm],
  628.         [L2|Lx],[W2|Wx],[F2|Fx]) :-
  629.     delete_replicate_literal_3(L1,Lm,Wm,Fm,Lx,Wx,Fx).
  630.      delete_replicate_literal_3(_,[],[],[],[],[],[]).
  631.  
  632. %%% Find minimum clause size for priority for a clause.
  633. %%% If all literal size asserted, clause size is clause_size_sp.
  634. %%% Otherwise, clause size is minliteral_size.
  635.      min_clausesize_sp(C,S) :-
  636.     size_by_clause,
  637.     clause_size_sp(C,S), !.
  638.      min_clausesize_sp(C,S) :-
  639.     minliteral_size(C,S).
  640.  
  641. %%% Find minimal literal size.
  642.      minliteral_size([L|Ls],S2) :-
  643.     literal_size(L,S1),
  644.     minliteral_size(Ls,S1,S2).
  645.      minliteral_size([L|Ls],S1,S2) :-
  646.     literal_size(L,X),
  647.     minimum(X,S1,Y),
  648.     minliteral_size(Ls,Y,S2).
  649.      minliteral_size([],S2,S2).
  650.  
  651. %%% Find minimum clause depth.
  652.      min_clause_depth([L|Ls],D2) :-
  653.     literal_depth(L,D1),
  654.     min_clause_depth(Ls,D1,D2).
  655.      min_clause_depth([L|Ls],D1,D2) :-
  656.     literal_depth(L,X),
  657.     minimum(X,D1,Y),
  658.     min_clause_depth(Ls,Y,D2).
  659.      min_clause_depth([],D2,D2).
  660.  
  661. %%% Rename sent_c to sent_C.
  662. %%% Assert at the end.
  663.      sentc_to_sentC_z :- not(not(sentc_to_sentC_z_1)).
  664.      sentc_to_sentC_z_1 :-
  665.     retract(sent_c(C)),
  666.     assertz(sent_C(C)),
  667.     fail.
  668.      sentc_to_sentC_z_1.
  669.  
  670. %%% Rename sent_c to sent_C.
  671. %%% Asser in the front.
  672.      sentc_to_sentC_a :- not(not(sentc_to_sentC_a_1)).
  673.      sentc_to_sentC_a_1 :-
  674.     retract(sent_c(C)),
  675.     asserta(sent_C(C)),
  676.     fail.
  677.      sentc_to_sentC_a_1.
  678.  
  679. %%% Rename sent_HM to sent_C.
  680. %%% Asser in the front.
  681.      sentHM_to_sentC_a :-
  682.          not(not(sentHM_to_sentC_a_1)).
  683.      sentHM_to_sentC_a_1 :-
  684.     retract(sent_HM(C1)),
  685.     asserta(sent_C(C1)),
  686.     fail.
  687.      sentHM_to_sentC_a_1.
  688.  
  689. %%% Succeed for horn clause.
  690.      horn_clause([X|Xs]) :-
  691.     negative_lit(X),
  692.     !, horn_clause(Xs).
  693.      horn_clause([X|Xs]) :-
  694.     !, negclause(Xs).
  695.      horn_clause([]).
  696.  
  697. %%% Separate a ground literal and the rest. Fails if no ground literals.
  698.      sep_gr_lit_2([W1|Ws1],[L1|Ls1],W1,Ws1,L1,Ls1) :-
  699.         var(W1), !.
  700.      sep_gr_lit_2([W|Ws],[L|Ls],W1,[W|Ws1],L1,[L|Ls1]) :-
  701.         sep_gr_lit_2(Ws,Ls,W1,Ws1,L1,Ls1), !.
  702.  
  703. %%% Separate a ground literal and the rest. Fails if no ground literals.
  704.      sep_gr_lit_3([W1|Ws1],[L1|Ls1],[T1|Ts1],W1,Ws1,L1,Ls1,T1,Ts1) :-
  705.         var(W1), !.
  706.      sep_gr_lit_3([W|Ws],[L|Ls],[T|Ts],W1,[W|Ws1],L1,[L|Ls1],T1,[T|Ts1]) :-
  707.         sep_gr_lit_3(Ws,Ls,Ts,W1,Ws1,L1,Ls1,T1,Ts1), !.
  708.  
  709. %%% Separate a ground literal and the rest. Fails if no ground literals.
  710.      sep_gr_lit_4([W1|Ws1],[L1|Ls1],[D1|Ds1],[T1|Ts1],W1,Ws1,L1,Ls1,
  711.         D1,Ds1,T1,Ts1) :-
  712.         var(W1), !.
  713.      sep_gr_lit_4([W|Ws],[L|Ls],[D|Ds],[T|Ts],W1,[W|Ws1],L1,[L|Ls1],
  714.         D1,[D|Ds1],T1,[T|Ts1]) :-
  715.         sep_gr_lit_4(Ws,Ls,Ds,Ts,W1,Ws1,L1,Ls1,D1,Ds1,T1,Ts1), !.
  716.  
  717. %%% Compute the number of non-ground literals. 
  718.      compute_V_lits([W|W2],N1,V2) :-  
  719.         \+ var(W), NN1 is N1 + 1, !, compute_V_lits(W2,NN1,V2).
  720.      compute_V_lits([_|W2],N1,V2) :-
  721.         !, compute_V_lits(W2,N1,V2).
  722.      compute_V_lits([],N1,N1).
  723.  
  724. %%% Union two lists.
  725.      union_lists([1|L1],[_|L2],[1|L3]) :- !, union_lists(L1,L2,L3).
  726.      union_lists([_|L1],[X|L2],[X|L3]) :- !, union_lists(L1,L2,L3).
  727.      union_lists([],_,[]).
  728.  
  729. %%% Check for duplicate clause in sent_C.
  730.      duplicate_clause_C(CSize,C,V) :-
  731.     not(not(duplicate_clause_C_1(CSize,C,V))),
  732.     !.
  733.      duplicate_clause_C_1(CSize,C,V) :-
  734.     const_list(V),
  735.     sent_C(cl(CSize,_,by(C,V11,V11,V,_),_,_,_,_,_,_)),
  736.     !.
  737.  
  738. %%%
  739. %%% instance_clause_C(C,V)
  740. %%%   input
  741. %%%     C : clause
  742. %%%     V : variables in C
  743. %%%   exceptions
  744. %%%     fails if C is not an instance of a sent_C clause
  745.      instance_clause_C(C,V) :-
  746.     not(not(instance_clause_C_1(C,V))).
  747.      instance_clause_C_1(C,V) :-
  748.     const_list(V),
  749.     sent_C(cl(_,_,by(C,V11,V11,_,_),_,_,_,_,_,_)),
  750.     !.
  751.  
  752. %%% Erase a clause from sent_C.
  753.      erase_clause_C(Csize,C,V) :-
  754.     not(not(erase_clause_C_1(Csize,C,V))),
  755.     !.
  756.      erase_clause_C_1(CSize,C,V) :-
  757.     const_list(V),
  758.     retract(sent_C(cl(CSize,_,by(C,V11,V11,V,_),_,_,_,_,_,_))),
  759.     !.
  760.      erase_clause_C_1(_,_,_).
  761.  
  762. %%% Logically erase a clause from sent_C.
  763.      logically_erase_clause_C(Csize,C,V) :-
  764.     not(not(logically_erase_clause_C_1(Csize,C,V))),
  765.     !.
  766.      logically_erase_clause_C_1(CSize,C,V) :-
  767.     const_list(V),
  768.     clause(sent_C(cl(CSize,_,by(C,V11,V11,V,_),_,_,_,_,_,_)),true,Ref),
  769.     not(logically_erased(sent_C,Ref)),
  770.     logically_erase(sent_C,Ref),
  771.     !.
  772.      logically_erase_clause_C_1(_,_,_).
  773.  
  774. %%% Erase a clause from sent_HM.
  775.      erase_clause_HM(Csize,C,V) :-
  776.     not(not(erase_clause_HM_1(Csize,C,V))),
  777.     !.
  778.      erase_clause_HM_1(CSize,C,V) :-
  779.     const_list(V),
  780.     retract(sent_HM(cl(CSize,_,by(C,V11,V11,V,_),_,_,_,_,_,_))),
  781.     !.
  782.      erase_clause_HM_1(_,_,_).
  783.  
  784. %%% Erase a clause from sent_T.
  785.      erase_clause_T(Csize,C,V) :-
  786.     not(not(erase_clause_T_1(Csize,C,V))),
  787.     !.
  788.      erase_clause_T_1(CSize,C,V) :-
  789.     const_list(V),
  790.     retract(sent_T(cl(CSize,_,by(C,V11,V11,V,_),_,_,_,_,_,_))),
  791.     !.
  792.      erase_clause_T_1(_,_,_).
  793.  
  794. %%% Logically erase a clause from sent_C only if it is non-input and its
  795. %%% priority excceeds the priority bound.
  796.      logically_erase_clause_C_prio(Csize,C,V) :-
  797.     not(not(logically_erase_clause_C_prio_1(Csize,C,V))),
  798.     !.
  799.      logically_erase_clause_C_prio_1(CSize,C,V) :-
  800.     const_list(V),
  801.     sent_C(cl(CSize,_,by(C,V11,V11,V,_),0,_,_,_,_,pr(_,_,_,_,P))),
  802.     priority_bound(PrioBound),
  803.     P>PrioBound,
  804.     clause(sent_C(cl(CSize,_,by(C,V11,V11,V,_),0,_,_,_,_,_)),true,Ref),
  805.     not(logically_erased(sent_C,Ref)),
  806.     logically_erase(sent_C,Ref),
  807.     !.
  808.      logically_erase_clause_C_prio_1(_,_,_).
  809.  
  810. %%% Erase a clause from sent_HM only if it is non-input and its priority
  811. %%% exceeds the priority bound.
  812.      erase_clause_HM_prio(Csize,C,V) :-
  813.     not(not(erase_clause_HM_prio_1(Csize,C,V))),
  814.     !.
  815.      erase_clause_HM_prio_1(CSize,C,V) :-
  816.     const_list(V),
  817.     sent_HM(cl(CSize,_,by(C,V11,V11,V,_),0,_,_,_,_,pr(_,_,_,_,P))),
  818.     priority_bound(PrioBound),
  819.     P>PrioBound,
  820.     retract(sent_HM(cl(CSize,_,by(C,V11,V11,V,_),0,_,_,_,_,_))),
  821.     !.
  822.      erase_clause_HM_prio_1(_,_,_).
  823.  
  824. %%% Erase a clause from sent_T only if it is non-input and its priority
  825. %%% exceeds the priority bound.
  826.      erase_clause_T_prio(Csize,C,V) :-
  827.     not(not(erase_clause_T_prio_1(Csize,C,V))),
  828.     !.
  829.      erase_clause_T_prio_1(CSize,C,V) :-
  830.     const_list(V),
  831.     sent_T(cl(CSize,_,by(C,V11,V11,V,_),0,_,_,_,_,pr(_,_,_,_,P))),
  832.     priority_bound(PrioBound),
  833.     P>PrioBound,
  834.     retract(sent_T(cl(CSize,_,by(C,V11,V11,V,_),0,_,_,_,_,_))),
  835.     !.
  836.      erase_clause_T_prio_1(_,_,_).
  837.  
  838. %%% Find the reference of a rewrite rule.
  839.      rewrite_rule_ref(Rule,Ref) :-
  840.     not(not(rewrite_rule_ref_1(Rule))),
  841.     retract(rrr_temp(Ref)),
  842.     !.
  843.      rewrite_rule_ref_1(rwr(R,var(V1,V1,V),F,U)) :-
  844.     const_list(V),
  845.     clause(rwr(R,var(V1,V1,V),F,U),true,Ref),
  846.         asserta(rrr_temp(Ref)),
  847.     !.
  848.  
  849. %%% Check if two clauses are duplicates.
  850.      duplicate_clauses(C1,C2) :-
  851.     asserta(dc_temp(C1)),
  852.     retract(dc_temp(C1a)),
  853.     not(not(duplicate_clauses_1(C1a,C2))),
  854.     !.
  855.      duplicate_clauses_1(C1,C2) :-
  856.     vars_tail(C1,V1),
  857.     vars_tail(C2,V2),
  858.     const_list(V1),
  859.     const_list(V2),
  860.     C1==C2.
  861.  
  862. %%% Check if a repeate replace rule has already been asserted.
  863.      duplicate_repeated_replace_rule(C,V) :-
  864.     not(not(duplicate_repeated_replace_rule_1(C,V))),
  865.     !.
  866.      duplicate_repeated_replace_rule_1(C,V) :-
  867.     const_list(V),
  868.     replace_rule_1(C,V,_,_,_),
  869.         !.
  870.  
  871. %%% Check if a once replace rule has already been asserted.
  872.      duplicate_once_replace_rule(C,V) :-
  873.     not(not(duplicate_once_replace_rule_1(C,V))),
  874.     !.
  875.      duplicate_once_replace_rule_1(C,V) :-
  876.     const_list(V),
  877.     replace_rule_2(C,V,_,_,_),
  878.         !.
  879.  
  880. %%% Check for a unit conflict with sent_C.
  881.      check_unit_conflict_C(U) :-
  882.     not(not(check_unit_conflict_C_1(U))).
  883.      check_unit_conflict_C_1(U) :-
  884.     negate(U,Un),
  885.     sent_C(cl(_,_,by([Un],V1,V2,_,_),_,_,_,_,_,_)),
  886.     unify_lists(V1,V2),
  887.     !.
  888.  
  889. %%% Check for a unit conflict with sent_HM.
  890.      check_unit_conflict_HM(U) :-
  891.     not(not(check_unit_conflict_HM_1(U))).
  892.      check_unit_conflict_HM_1(U) :-
  893.     negate(U,Un),
  894.     sent_HM(cl(_,_,by([Un],V1,V2,_,_),_,_,_,_,_,_)),
  895.     unify_lists(V1,V2),
  896.     !.
  897.